Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__dbl(0)  → 0
2:    a__dbl(s(X))  → s(s(dbl(X)))
3:    a__dbls(nil)  → nil
4:    a__dbls(cons(X,Y))  → cons(dbl(X),dbls(Y))
5:    a__sel(0,cons(X,Y))  → mark(X)
6:    a__sel(s(X),cons(Y,Z))  → a__sel(mark(X),mark(Z))
7:    a__indx(nil,X)  → nil
8:    a__indx(cons(X,Y),Z)  → cons(sel(X,Z),indx(Y,Z))
9:    a__from(X)  → cons(X,from(s(X)))
10:    mark(dbl(X))  → a__dbl(mark(X))
11:    mark(dbls(X))  → a__dbls(mark(X))
12:    mark(sel(X1,X2))  → a__sel(mark(X1),mark(X2))
13:    mark(indx(X1,X2))  → a__indx(mark(X1),X2)
14:    mark(from(X))  → a__from(X)
15:    mark(0)  → 0
16:    mark(s(X))  → s(X)
17:    mark(nil)  → nil
18:    mark(cons(X1,X2))  → cons(X1,X2)
19:    a__dbl(X)  → dbl(X)
20:    a__dbls(X)  → dbls(X)
21:    a__sel(X1,X2)  → sel(X1,X2)
22:    a__indx(X1,X2)  → indx(X1,X2)
23:    a__from(X)  → from(X)
There are 14 dependency pairs:
24:    A__SEL(0,cons(X,Y))  → MARK(X)
25:    A__SEL(s(X),cons(Y,Z))  → A__SEL(mark(X),mark(Z))
26:    A__SEL(s(X),cons(Y,Z))  → MARK(X)
27:    A__SEL(s(X),cons(Y,Z))  → MARK(Z)
28:    MARK(dbl(X))  → A__DBL(mark(X))
29:    MARK(dbl(X))  → MARK(X)
30:    MARK(dbls(X))  → A__DBLS(mark(X))
31:    MARK(dbls(X))  → MARK(X)
32:    MARK(sel(X1,X2))  → A__SEL(mark(X1),mark(X2))
33:    MARK(sel(X1,X2))  → MARK(X1)
34:    MARK(sel(X1,X2))  → MARK(X2)
35:    MARK(indx(X1,X2))  → A__INDX(mark(X1),X2)
36:    MARK(indx(X1,X2))  → MARK(X1)
37:    MARK(from(X))  → A__FROM(X)
The approximated dependency graph contains one SCC: {24-27,29,31-34,36}.
Tyrolean Termination Tool  (17.05 seconds)   ---  May 3, 2006